基于开关信号理论的四值ECL电路

从一个有效的多值代数系统应能反映多值电路中的物理过程的这一原则出发,本文提出了一组可以描写多值ECL电路中信号与开关元件间相互作用的运算。讨论了这些运算的物理对应及有关性质,并由此建立了适用于ECL电路的开关信号理论。本文设计了若干基本四值ECL电路,用SPICE程序模拟证明了它们均具有正确的逻辑功能与理想的DC特性。     

Operational concepts of nonmonotonic logics part 1: Default logic

We give an introduction to default logic, one of the most prominent nonmonotonic logics. Emphasis is given to providing an operational interpretation for the semantics of default logic that is usually defined by fixed-point concepts (extensions). We introduce a process model that allows to exactly calculate the extensions of a default theory in a quite easy way. We give a prototypical implementation of processes in Prolog able to handle the examples that can be found in literature. Finally, we develop some theoretical results about default logic and give new simple proofs using the process model as a theoretical tool.     

Autoepistemic logic of first order and its expressive power

We study the expressive power of first-order autoepistemic logic. We argue that full introspection of rational agents should be carried out by minimizing positive introspection and maximizing negative introspection. Based on full introspection, we propose the maximal well-founded semantics that characterizes autoepistemic reasoning processes of rational agents, and show that breadth of the semantics covers all theories in autoepistemic logic of first order, Moore's AE logic, and Reiter's default logic. Our study demonstrates that the autoepistemic logic of first order is a very powerful framework for nonmonotonic reasoning, logic programming, deductive databases, and knowledge representation.This research is partially supported by NSERC grant OGP42193.     

On isomorphic formalisations

Previous research into the formalisation of statute law identified a number of uses of language which posed problems for formalisation. A previous paper argued that these uses establish the requirement that a formalisation be isomorphic, but noted that this has odd consequences. This paper expands on what these consequences are and argues that they undermine the very idea of formalisation. Therefore, the whole argument constitutes a reductio ad absurdum of the idea of formalising statute law. The paper provides reasons why this activity is impossible and places the conclusion in the context of the development of modem logic, in which context it appears uncontroversial.     

A temporal logic approach to object certification

A brief overview is made of the use of temporal logic formalisms for specifying and verifying concurrent systems in general and information systems in particular. The requirements imposed by object-orientation on such formalisms are examined. A logic is proposed fulfilling those requirements (except concerning non-monotonic features), allowing the uniform treatment of both local and global properties of systems with concurrent, interacting components organized in classes, and supporting specialization. A semantics and a calculus (following an axiomatic, Hilbert style) are presented in detail. The calculus includes rules for the sound inheritance and reflection of theorems between classes. Practical aspects of the usage of such a logic for both specification and verification are considered. To this end a set of metatheorems is provided for expediting the proof of invariants. Finally, the need and availability of automatic theorem proving for systems querying is briefly discussed.     

可编程控制器和变频器在改造在用电梯自动控制系统中的应用

介绍采用三菱FX2系列可编程控制器(PLC)和FR-V240E系列变频器改造老式电梯控制系统的系统构成、应用技术以及设计方法.     

Decision learning about production control as machines break down in a flexible manufacturing system

During manufacturing, there are many situations that can affect production performance. Such situations include machine breakdowns, rush orders, order changes, and order delays. When such issues occur, one has to make decisions to try to maintain production efficiency.Human decisions tend to be too late and incomplete in such contingencies. Thus a system that can make better decisions in time to maintain production performance is needed. To achieve this objective, the intelligent decision system described in this paper integrates artificial intelligence, an optimization technique, and simulation to solve such problems. The decision-making logic of the intelligent decision system is described by event graphs. It imitates the manner of human thinking.Self-learning of the decision-making process is used to strengthen the decision quality. In this study, a method of rule induction is applied to build up the self-learning system. There are two subsystems included in this system. One is rule generation and the other is knowledge management. A case for machine breakdowns is presented and discussed. A series of tests designed to validate the self-learning system are presented. These demonstrate that a rule induction method is suitable for constructing the self-learning.     

Symmetry and model checking

We show how to exploit symmetry in model checking for concurrent systems containing many identical or isomorphic components. We focus in particular on those composed of many isomorphic processes. In many cases we are able to obtain significant, even exponential, savings in the complexity of model checking.The author's work was supported in part by NSF Grant CCR 941-5496, Semiconductor Research Corporation Contract 95-DP-388, and Texas Advanced Technology Program Grant 003658-250.The author's work was supported in part by NSF Grant CCR-9212183.